Section: New Results

A formal description of exact real arithmetic

Participants : Yves Bertot, Nicolas Magaud [University of Strasbourg] .

We revisited an old package available in the contributions to the Coq system, where algorithms to perform real number computations were described. This package was using primitives described using axioms. We showed that these axioms were faulty and proposed solutions to salvage the package and make it more safely usable in the future.